package test;

import resolution.Resolution;
import base.Atome;
import base.Et;
import base.Formule;
import base.Implique;
import base.Non;
import base.PourTout;
import base.Variable;

public class Lanceur {

	/**
	 * @param args
	 */
	public static void main(String[] args) {

		// ///////////////////////////////////////////////////////////////
		// Exemple 1 : (avec plusieurs premisses distinctes)
		//
		// 1. Aucun avare n'est altruiste
		// 2. Les personnes qui conservent les coquilles d'oeufs sont avares
		// Donc: aucune personne altruiste ne conserve les coquilles d'oeufs
		// ///////////////////////////////////////////////////////////////

		System.out.println();
		System.out.println("****************************************************************************");
		System.out.println();
		System.out.println("Exemple 1 (pris dans le cours): (avec plusieurs premisses distinctes)");
		System.out.println();
		System.out.println("1. Aucun avare n'est altruiste");
		System.out.println("2. Les personnes qui conservent les coquilles d'oeufs sont avares");
		System.out.println("Donc: aucune personne altruiste ne conserve les coquilles d'oeufs");
		System.out.println();

		// Prémisses 1 : Aucun avare n'est altruiste
		Variable x = new Variable("x");
		Atome al1 = new Atome("al", x);
		Non nAl = new Non(al1);
		Atome avx1 = new Atome("av", x);
		Implique impl = new Implique(avx1, nAl);
		PourTout p1 = new PourTout(x, impl);

		// Prémisses 2 : Les personnes qui conservent les coquilles d'oeufs sont
		// avares
		Atome oeufx1 = new Atome("oeuf", x);
		Atome avx2 = new Atome("av", x);
		Implique impl2 = new Implique(oeufx1, avx2);
		PourTout p2 = new PourTout(x, impl2);

		// Conclusion : Donc aucune personne altruiste ne conserve les coquilles
		// d'oeufs
		Atome oeufx2 = new Atome("oeuf", x);
		Atome al2 = new Atome("al", x);
		Non noeufx = new Non(oeufx2);
		Implique impl3 = new Implique(al2, noeufx);
		PourTout ccl = new PourTout(x, impl3);

		// Résolution
		Formule[] premisses1 = { p1, p2 };
		new Resolution(premisses1, ccl);

		// ////////////////////////////////////////////////////////////////////
		// Exemple 2 : (avec plusieurs prémisses réunit en une seule par des ET)
		//
		// 1. les bébés sont illogiques
		// 2. nul n'est méprisé quand il peut venir à bout d'un crocodile
		// 3. les gens illogiques sont méprisés
		// Donc : les bébés ne peuvent venir à bout des crocodiles
		// ////////////////////////////////////////////////////////////////////

		System.out.println();
		System.out.println("****************************************************************************");
		System.out.println();
		System.out.println("Exemple 2 (donné par Mr Jussien) : (avec plusieurs prémisses réunit en une seule par des ET)");
		System.out.println();
		System.out.println("1. les bébés sont illogiques");
		System.out.println("2. nul n'est méprisé quand il peut venir à bout d'un crocodile");
		System.out.println("3. les gens illogiques sont méprisés");
		System.out.println("Donc : les bébés ne peuvent venir à bout des crocodiles");
		System.out.println();

		// Prémisses:
		// 1. les bébés sont illogiques
		// 2. nul n'est méprisé quand il peut venir à bout d'un crocodile
		// 3. les gens illogiques sont méprisés
		Formule premisses = new Et(new PourTout(new Variable("x"), new Implique(new Atome("bebe", new Variable("x")), new Atome("illogique", new Variable("x")))), new Et(new PourTout(new Variable("x"), new Implique(new Atome("crocodile", new Variable("x")), new Non(new Atome("meprise", new Variable("x"))))), new PourTout(new Variable("x"), new Implique(new Atome("illogique", new Variable("x")), new Atome("meprise", new Variable("x"))))));
		Formule[] premisses2 = { premisses };

		// Conclusion: Donc les bébés ne peuvent venir à bout des crocodiles
		Formule conclusion = new PourTout(new Variable("x"), new Implique(new Atome("bebe", new Variable("x")), new Non(new Atome("crocodile", new Variable("x")))));

		// Résolution
		new Resolution(premisses2, conclusion);
	}
}
